Values

Our programs will compute and return a single value. %%🖋 Edit in Excalidraw%% Values are closed expressions.

Transitions

We are going to use operational semantics. Our transition system will consist of rules:

• closed terms = states
• instruction transitions - perform computation
• search transitions - determine evaluation order %%🖋 Edit in Excalidraw%%

Multi-Step Transitions

%%🖋 Edit in Excalidraw%% Reflexive transitive closure of

Properties

Finality

%%🖋 Edit in Excalidraw%%

Determinism

%%🖋 Edit in Excalidraw%%

Evaluation

%%🖋 Edit in Excalidraw%%

Type Safety

%%🖋 Edit in Excalidraw%% Type safety theorem proof will be in exam.